ATS (langage de programmation)

ATS (Applied Type System) est un langage de programmation conçu pour unifier la programmation avec des spécifications formelles. ATS prend en charge la combinaison de la démonstration du théorème avec la programmation pratique grâce à l'utilisation de systèmes de type avancés. Une version antérieure de The Computer Language Benchmarks Game a démontré que les performances d'ATS sont comparables à celles des langages de programmation C et C++. En utilisant la preuve de théorème et la vérification de type stricte, le compilateur peut détecter et prouver que ses fonctions implémentées ne sont pas sensibles aux bogues tels que la division par zéro, les fuites de mémoire, le dépassement de mémoire tampon et d'autres formes de corruption de mémoire en vérifiant l' arithmétique du pointeur et le comptage de références avant que le programme se compile. De plus, en utilisant le système de démonstration de théorème intégré de l'ATS (ATS / LF), le programmeur peut utiliser des constructions statiques qui sont entrelacées avec le code opérationnel pour prouver qu'une fonction atteint sa spécification.

Histoire

ATS est principalement dérivé des langages de programmation ML et OCaml. Une langue antérieure, Dependent ML, du même auteur a été incorporée par la langue.

La dernière version d'ATS1 (Anairiats) est sortie en v0.2.12 le 20/01/2015. La première version d'ATS2 (Postiats) est sortie en septembre 2013

Preuve du théorème

L'objectif principal de l'ATS est de soutenir la démonstration de théorèmes en combinaison avec une programmation pratique. Avec la démonstration d'un théorème, on peut prouver, par exemple, qu'une fonction implémentée ne produit pas de fuites de mémoire. Cela évite également d'autres bogues qui, autrement, ne pourraient être trouvés que pendant les tests. Il incorpore un système similaire à ceux des assistants de preuve qui visent généralement uniquement à vérifier les preuves mathématiques, sauf que ATS utilise cette capacité pour prouver que les implémentations de ses fonctions fonctionnent correctement et produisent le résultat attendu.

À titre d'exemple simple, dans une fonction utilisant la division, le programmeur peut prouver que le diviseur ne sera jamais égal à zéro, empêchant une Division par zéro. Disons que le diviseur «X» a été calculé comme 5 fois la longueur de la liste «A». On peut prouver que dans le cas d'une liste non vide, «X» est non nul, puisque «X» est le produit de deux nombres non nuls (5 et la longueur de «A»). Un exemple plus pratique serait de prouver par le comptage de références que le compte de rétention sur un bloc de mémoire alloué est correctement compté pour chaque pointeur. On peut alors savoir, et prouver littéralement, que l'objet ne sera pas désalloué prématurément, et que les fuites de mémoire ne se produiront pas.

L'avantage du système ATS est que puisque toute démonstration de théorème se produit strictement dans le compilateur, cela n'a aucun effet sur la vitesse du programme exécutable. Le code ATS est souvent plus difficile à compiler que le code C standard, mais une fois qu'il est compilé, le programmeur peut être certain qu'il s'exécute correctement au degré spécifié par leurs preuves (en supposant que le compilateur et le système d'exécution sont corrects).

Dans ATS, les preuves sont distinctes de l'implémentation, il est donc possible d'implémenter une fonction sans la prouver si le programmeur le souhaite.

Représentation des données

Selon l'auteur (Hongwei Xi), l'efficacité d'ATS est en grande partie due à la façon dont les données sont représentées dans le langage et aux optimisations de fin d'appel (qui sont généralement importantes pour l'efficacité des langages de programmation fonctionnels). Les données peuvent être stockées dans une représentation plate ou non encadrée plutôt que dans une représentation encadrée.

Preuve du théorème: un cas d'introduction

Propositions

dataprop exprime les prédicats sous forme de types algébriques.

Exemple de prédicats en pseudo-code assez similaire à la source ATS (voir ci-dessous pour une source ATS valide) pour la fonction factorielle, dont le nom est abrégé en « FACT » :

 FACT(n, r) ssi fact(n) = r
 MUL(n, m, prod) ssi n * m = prod
 
 FACT(n, r) = 
     FACT(0, 1) 
   | FACT(n, r) ssi FACT(n-1, r1) et MUL(n, r1, r) // pour n> 0
 
 // exprime le fact(n) = r ssi r = n * r1 et r1 = fact(n-1)

En code ATS :

 dataprop FACT (int, int) =
  | FACTbas (0, 1)       // basic case: FACT(0, 1)
  | {n:int | n > 0} {r,r1:int} // inductive case
    FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r))

où FACT (int, int) est un type de preuve

Exemple

Factoriel non récursif avec proposition ou " Théorème " prouvant à travers la construction dataprop.

L'évaluation de fact1 (n-1) renvoie une paire (proof_n_minus_1 | result_of_n_minus_1) qui est utilisée dans le calcul de fact1 (n). Les preuves expriment les prédicats de la proposition.

Partie 1 (algorithme et propositions)

[FACT (n, r)] implique [fact (n) = r]
 [MUL (n, m, prod)] implique [n * m = prod]

FAIT (0, 1)
 FACT (n, r) ssi FACT (n-1, r1) et MUL (n, r1, r) pour tout n> 0

Se souvenir:

{...} quantification universelle
[...] quantification existentielle
(... | ...) (preuve | valeur)
@ (...) tuple plat ou tuple de paramètres de fonction variadique
. <...>. métrique de terminaison 

#include "share/atspre_staload.hats"

dataprop FACT (int, int) =
 | FACTbas (0, 1) of () // basic case
 | {n:nat}{r:int}    // inductive case
  FACTind (n+1, (n+1)*r) of (FACT (n, r))

(* note that int(x), also int x, is the monovalued type of the int x value.

 The function signature below says:
 forall n:nat, exists r:int where fact( num: int(n)) returns (FACT (n, r) | int(r)) *)

fun fact{n:nat} .<n>. (n: int (n)) : [r:int] (FACT (n, r) | int(r)) =
(
 ifcase
 | n > 0 => ((FACTind(pf1) | n * r1)) where 
 { 
  val (pf1 | r1) = fact (n-1)
 }
 | _(*else*) => (FACTbas() | 1)
)

Partie 2 (routines et test)

implement main0 (argc, argv) =
{
 val () = if (argc != 2) then prerrln! ("Usage: ", argv[0], " <integer>")

 val () = assert (argc >= 2)
 val n0 = g0string2int (argv[1])
 val n0 = g1ofg0 (n0)
 val () = assert (n0 >= 0)
 val (_(*pf*) | res) = fact (n0)

 val ((*void*)) = println! ("fact(", n0, ") = ", res)
}

Tout cela peut être ajouté à un seul fichier et compilé comme suit. La compilation devrait fonctionner avec divers compilateurs C back-end, par exemple gcc . Le nettoyage de la mémoire n'est pas utilisé sauf indication explicite avec -D_ATS_GCATS)

$ patscc fact1.dats -o fact1
$ ./fact1 4

compile et donne le résultat attendu

Types de base

• booléen (vrai, faux)
• int (littéraux: 255, 0377, 0xFF), unaire moins comme ~ (comme dans ML)
• double
• char 'a'
• chaîne "abc"

Tuples et disques

préfixe @ ou aucun signifie allocation directe, plate ou sans boîte

 val x : @(int, char) = @(15, 'c') // x.0 = 15 ; x.1 = 'c'
 val @(a, b) = x          // pattern matching binding, a= 15, b='c'
 val x = @{first=15, second='c'}  // x.first = 15
 val @{first=a, second=b} = x    // a= 15, b='c'
 val @{second=b, ...} = x      // with omission, b='c'

préfixe 'signifie allocation indirecte ou encadrée

 val x : '(int, char) = '(15, 'c') // x.0 = 15 ; x.1 = 'c'
 val '(a, b) = x          // a= 15, b='c'
 val x = '{first=15, second='c'}  // x.first = 15
 val '{first=a, second=b} = x    // a= 15, b='c'
 val '{second=b, ...} = x      // b='c'

spécial

Avec '|' comme séparateur, certaines fonctions renvoient la valeur du résultat encapsulée avec une évaluation des prédicats

val (predicate_proofs | values) = mes paramètres

Commun

{...} quantification universelle
[...] quantification existentielle
(...) expression entre parenthèses ou tuple

(... | ...) (preuves | valeurs)

. <...>. métrique de terminaison

@ (...) tuple plat ou tuple de paramètres de fonction variadique (voir l'exemple printf)

@ [byte] [BUFLEN] type d'un tableau de valeurs BUFLEN de type octet 
@ [byte] [BUFLEN] () instance de tableau
@ [byte] [BUFLEN] (0) tableau initialisé à 0

dictionnaire

sorte

domaine

 sortdef nat = {a: int | a >= 0 }   // from prelude: ∀ ''a'' ∈ int ...

 typedef String = [a:nat] string(a)  // [..]: ∃ ''a'' ∈ nat ...

type (comme tri)

tri générique pour les éléments de la longueur d'un mot pointeur, à utiliser dans les fonctions polymorphes paramétrées par type. Également "types en boîte" .

taper

version linéaire du type précédent avec longueur abstraite. Également des types non emballés.

viewtype

une classe de domaine comme type avec une vue (association de mémoire)

viewt @ ype

version linéaire du type de vue avec une longueur abstraite. Il remplace le type de vue

vue

relation d'un Type et d'un emplacement mémoire. L'infixe @ est son constructeur le plus courant

T @ L affirme qu'il existe une vue de type T à l'emplacement L

 fun {a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): @(a @ l | a)
 
 fun {a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): @(a @ l | void)

le type de ptr_get0 (T) est ∀ l : adr. (T @ l | ptr (l)) → (T @ l | T) // voir manuel, section 7.1. Accès sécurisé à la mémoire via des pointeurs

viewdef array_v (a: viewt @ ype, n: int, l: addr) = @ [a] [n] @ l

T?

type éventuellement non initialisé

l'exhaustivité de la correspondance des modèles

comme dans le cas +, val +, type +, viewtype +,. . .

• avec le suffixe '+' le compilateur émet une erreur en cas d'alternatives non exhaustives
• sans suffixe, le compilateur émet un avertissement
• avec '-' comme suffixe, évite le contrôle d'exhaustivité

 staload "foo.sats" // foo.sats is loaded and then opened into the current namespace

 staload F = "foo.sats" // to use identifiers qualified as $F.bar

 dynload "foo.dats" // loaded dynamically at run-time

vue de données

Les vues de données sont souvent déclarées pour encoder des relations définies de manière récursive sur des ressources linéaires.

dataview array_v (a: viewt @ ype +, int, addr) = | {l: addr} array_v_none (a, 0, l) | {n: nat} {l: addr} array_v_some (a, n + 1, l) of (a @ l, array_v (a, n, l + sizeof a))

type de données / type de vue de données

Types de données

type de données jour ouvrable = Mon | Tue | Mer | Thu | ven

listes

type de données list0 (a: t @ ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)

dataviewtype

Un type de vue de données est similaire à un type de données, mais il est linéaire. Avec un dataviewtype, le programmeur est autorisé à libérer explicitement (ou désallouer) de manière sûre la mémoire utilisée pour stocker les constructeurs associés au dataviewtype.

variables

variables locales

var res: int avec pf_res = 1 // introduit pf_res comme alias de view @ (res)

sur l' allocation de tableau de pile:

#define BUFLEN 10
var! p_buf avec pf_buf = @ [octet] [BUFLEN] (0) // pf_buf = @ [octet] [BUFLEN] (0) @ p_buf 

Voir les déclarations val et var

Liens externes

• Page d'accueil ATS
• La documentation du langage de programmation ATS pour ATS2
• Ancienne documentation du langage de programmation ATS pour ATS1
• Brouillon du manuel (obsolète). Certains exemples font référence à des fonctionnalités ou des routines non présentes dans la version (Anairiats-0.1.6) (par exemple: surcharge d'impression pour strbuf, et l'utilisation de ses exemples de tableau donne des erreurs comme "l'utilisation de l'abonnement au tableau n'est pas prise en charge".)
• ATS pour les programmeurs ML
• Exemples d'apprentissage et courts cas d'utilisation de l'ATS